Search Results

Documents authored by Lewis, S. E.



Lewis, S. E.

Document
NLP and Phenotypes: using Ontologies to link Human Diseases to Animal Models

Authors: N. Washington, M. Gibson, C.J. Mungall, Michael Ashburner, G. Gkoutos, M. Westerfield, M. Haendel, and S. E. Lewis

Published in: Dagstuhl Seminar Proceedings, Volume 8131, Ontologies and Text Mining for Life Sciences : Current Status and Future Perspectives (2008)


Abstract
The path to disease gene discovery in humans is often a lengthy one, but can be significantly shortened if links between human and model organism phenotypes are readily available. Collecting and storing these descriptions in a common resource, recorded with ontologies, as well as developing the tools for annotation, access, and analysis are among the goals of the National Center for Biomedical Ontology. The use of well-structured, expert-reviewed ontologies during curation allows biological data to be understandable by both humans and computers, and thereby increases the capacity for meaningful analysis. We have developed the EQ annotation model, which uses ontology terms to label and link together entities, such as anatomical structures, with the qualities describing them. Phenotypes are represented in our model using any combination of entity (such as anatomy) ontologies in combination with an ontology of qualities (PATO). Together with the model organism databases Zfin and FlyBase, we are evaluating this model, using the Phenote Annotation Tool to capture the mutant phenotypes of 200 genes known to cause human disease (from OMIM records) that have corresponding fly and zebrafish mutant phenotypes. The phenotypic data modeled in this way is available from the NCBO Open Biomedical Database (OBD), which has the same underlying annotation data model, and can currently be accessed via a computational (REST) interface for utilization by other external application or databases. This work is funded by the NIH.

Cite as

N. Washington, M. Gibson, C.J. Mungall, Michael Ashburner, G. Gkoutos, M. Westerfield, M. Haendel, and S. E. Lewis. NLP and Phenotypes: using Ontologies to link Human Diseases to Animal Models. In Ontologies and Text Mining for Life Sciences : Current Status and Future Perspectives. Dagstuhl Seminar Proceedings, Volume 8131, p. 1, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2008)


Copy BibTex To Clipboard

@InProceedings{washington_et_al:DagSemProc.08131.10,
  author =	{Washington, N. and Gibson, M. and Mungall, C.J. and Ashburner, Michael and Gkoutos, G. and Westerfield, M. and Haendel, M. and Lewis, S. E.},
  title =	{{NLP and Phenotypes: using Ontologies to link Human Diseases to Animal Models}},
  booktitle =	{Ontologies and Text Mining for Life Sciences : Current Status and Future Perspectives},
  pages =	{1--1},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2008},
  volume =	{8131},
  editor =	{Michael Ashburner and Ulf Leser and Dietrich Rebholz-Schuhmann},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DagSemProc.08131.10},
  URN =		{urn:nbn:de:0030-drops-15143},
  doi =		{10.4230/DagSemProc.08131.10},
  annote =	{Keywords: Phenotypes, ontologies, annotation}
}

Lewis, Richard

Document
Music Information Technology and Professional Stakeholder Audiences: Mind the Adoption Gap

Authors: Cynthia C.S. Liem, Andreas Rauber, Thomas Lidy, Richard Lewis, Christopher Raphael, Joshua D. Reiss, Tim Crawford, and Alan Hanjalic

Published in: Dagstuhl Follow-Ups, Volume 3, Multimodal Music Processing (2012)


Abstract
The academic discipline focusing on the processing and organization of digital music information, commonly known as Music Information Retrieval (MIR), has multidisciplinary roots and interests. Thus, MIR technologies have the potential to have impact across disciplinary boundaries and to enhance the handling of music information in many different user communities. However, in practice, many MIR research agenda items appear to have a hard time leaving the lab in order to be widely adopted by their intended audiences. On one hand, this is because the MIR field still is relatively young, and technologies therefore need to mature. On the other hand, there may be deeper, more fundamental challenges with regard to the user audience. In this contribution, we discuss MIR technology adoption issues that were experienced with professional music stakeholders in audio mixing, performance, musicology and sales industry. Many of these stakeholders have mindsets and priorities that differ considerably from those of most MIR academics, influencing their reception of new MIR technology. We mention the major observed differences and their backgrounds, and argue that these are essential to be taken into account to allow for truly successful cross-disciplinary collaboration and technology adoption in MIR.

Cite as

Cynthia C.S. Liem, Andreas Rauber, Thomas Lidy, Richard Lewis, Christopher Raphael, Joshua D. Reiss, Tim Crawford, and Alan Hanjalic. Music Information Technology and Professional Stakeholder Audiences: Mind the Adoption Gap. In Multimodal Music Processing. Dagstuhl Follow-Ups, Volume 3, pp. 227-246, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)


Copy BibTex To Clipboard

@InCollection{liem_et_al:DFU.Vol3.11041.227,
  author =	{Liem, Cynthia C.S. and Rauber, Andreas and Lidy, Thomas and Lewis, Richard and Raphael, Christopher and Reiss, Joshua D. and Crawford, Tim and Hanjalic, Alan},
  title =	{{Music Information Technology and Professional Stakeholder Audiences: Mind the Adoption Gap}},
  booktitle =	{Multimodal Music Processing},
  pages =	{227--246},
  series =	{Dagstuhl Follow-Ups},
  ISBN =	{978-3-939897-37-8},
  ISSN =	{1868-8977},
  year =	{2012},
  volume =	{3},
  editor =	{M\"{u}ller, Meinard and Goto, Masataka and Schedl, Markus},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DFU.Vol3.11041.227},
  URN =		{urn:nbn:de:0030-drops-34759},
  doi =		{10.4230/DFU.Vol3.11041.227},
  annote =	{Keywords: music information retrieval, music computing, domain expertise, technology adoption, user needs, cross-disciplinary collaboration}
}

Lewis, Matthew R.

Document
Casually Evolving Creative Technology Systems

Authors: Matthew R. Lewis

Published in: Dagstuhl Seminar Proceedings, Volume 9291, Computational Creativity: An Interdisciplinary Approach (2009)


Abstract
This position paper will describe the early stages of a development effort in which an interactive evolutionary design approach is being applied to the domain of technology-based system development, in a new media art and design context. These systems connect different technologies and techniques in order to process and transform data of one type into another. For example, location data might be used to select a relevant network information feed, the text of which drives geometry generation, which in turn could be sent to a 3D printer that would produce a sculpture. While the flexibility of this problem domain is idiosyncratic to our interdisciplinary new media environment, the target physical context for using a creativity support tool, and the context’s effect on creative output is rather the primary research focus. The goal is to explore the possibilities of what might be termed "casual design", analogous to the “casual gaming” genre in which games are played by anyone, where ever they might find a few spare minutes, rather than requiring significant time and hardware commitments.

Cite as

Matthew R. Lewis. Casually Evolving Creative Technology Systems. In Computational Creativity: An Interdisciplinary Approach. Dagstuhl Seminar Proceedings, Volume 9291, pp. 1-10, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2009)


Copy BibTex To Clipboard

@InProceedings{lewis:DagSemProc.09291.8,
  author =	{Lewis, Matthew R.},
  title =	{{Casually Evolving Creative Technology Systems}},
  booktitle =	{Computational Creativity: An Interdisciplinary Approach},
  pages =	{1--10},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2009},
  volume =	{9291},
  editor =	{Margaret Boden and Mark D'Inverno and Jon McCormack},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DagSemProc.09291.8},
  URN =		{urn:nbn:de:0030-drops-21951},
  doi =		{10.4230/DagSemProc.09291.8},
  annote =	{Keywords: Computational creativity}
}

Lewis, Robert Y.

Document
Formalized functional analysis with semilinear maps

Authors: Frédéric Dupuis, Robert Y. Lewis, and Heather Macbeth

Published in: LIPIcs, Volume 237, 13th International Conference on Interactive Theorem Proving (ITP 2022)


Abstract
Semilinear maps are a generalization of linear maps between vector spaces where we allow the scalar action to be twisted by a ring homomorphism such as complex conjugation. In particular, this generalization unifies the concepts of linear and conjugate-linear maps. We implement this generalization in Lean’s mathlib library, along with a number of important results in functional analysis which previously were impossible to formalize properly. Specifically, we prove the Fréchet-Riesz representation theorem and the spectral theorem for compact self-adjoint operators generically over real and complex Hilbert spaces. We also show that semilinear maps have applications beyond functional analysis by formalizing the one-dimensional case of a theorem of Dieudonné and Manin that classifies the isocrystals over an algebraically closed field with positive characteristic.

Cite as

Frédéric Dupuis, Robert Y. Lewis, and Heather Macbeth. Formalized functional analysis with semilinear maps. In 13th International Conference on Interactive Theorem Proving (ITP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 237, pp. 10:1-10:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)


Copy BibTex To Clipboard

@InProceedings{dupuis_et_al:LIPIcs.ITP.2022.10,
  author =	{Dupuis, Fr\'{e}d\'{e}ric and Lewis, Robert Y. and Macbeth, Heather},
  title =	{{Formalized functional analysis with semilinear maps}},
  booktitle =	{13th International Conference on Interactive Theorem Proving (ITP 2022)},
  pages =	{10:1--10:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-252-5},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{237},
  editor =	{Andronick, June and de Moura, Leonardo},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2022.10},
  URN =		{urn:nbn:de:0030-drops-167191},
  doi =		{10.4230/LIPIcs.ITP.2022.10},
  annote =	{Keywords: Functional analysis, Lean, linear algebra, semilinear, Hilbert space}
}
Document
Formalizing the Solution to the Cap Set Problem

Authors: Sander R. Dahmen, Johannes Hölzl, and Robert Y. Lewis

Published in: LIPIcs, Volume 141, 10th International Conference on Interactive Theorem Proving (ITP 2019)


Abstract
In 2016, Ellenberg and Gijswijt established a new upper bound on the size of subsets of F^n_q with no three-term arithmetic progression. This problem has received much mathematical attention, particularly in the case q = 3, where it is commonly known as the cap set problem. Ellenberg and Gijswijt’s proof was published in the Annals of Mathematics and is noteworthy for its clever use of elementary methods. This paper describes a formalization of this proof in the Lean proof assistant, including both the general result in F^n_q and concrete values for the case q = 3. We faithfully follow the pen and paper argument to construct the bound. Our work shows that (some) modern mathematics is within the range of proof assistants.

Cite as

Sander R. Dahmen, Johannes Hölzl, and Robert Y. Lewis. Formalizing the Solution to the Cap Set Problem. In 10th International Conference on Interactive Theorem Proving (ITP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 141, pp. 15:1-15:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)


Copy BibTex To Clipboard

@InProceedings{dahmen_et_al:LIPIcs.ITP.2019.15,
  author =	{Dahmen, Sander R. and H\"{o}lzl, Johannes and Lewis, Robert Y.},
  title =	{{Formalizing the Solution to the Cap Set Problem}},
  booktitle =	{10th International Conference on Interactive Theorem Proving (ITP 2019)},
  pages =	{15:1--15:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-122-1},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{141},
  editor =	{Harrison, John and O'Leary, John and Tolmach, Andrew},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2019.15},
  URN =		{urn:nbn:de:0030-drops-110703},
  doi =		{10.4230/LIPIcs.ITP.2019.15},
  annote =	{Keywords: formal proof, combinatorics, cap set problem, Lean}
}
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail